package it.polimi.loganalyzer.model;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Set;

public class PRISMGenerator {

	public static String getPrismModel(State initialState, State finalState, Set<State> states,
			Set<Transition> transitions) {

		
		String footer = "\nendmodule";

		HashMap<State, Integer> stateMap = new HashMap<State, Integer>();
		HashMap<State, List<Transition>> distributionMap = new HashMap<State, List<Transition>>();

		String labels = "";
		int variable = 0;

		for (State s : states) {
			stateMap.put(s, variable);
			labels += "label \"" + s.getName() + "\" = s=" + variable + ";\n";
			variable++;

			List<Transition> list = new ArrayList<Transition>();
			for (Transition t : transitions) {
				if (t.getSource().equals(s)){
					list.add(t);
				}
			}
			distributionMap.put(s, list);
		}
		
		String header = createHeader(states.size()-1, stateMap.get(initialState));
		String body = "\n";

		for (State s : states) {
			List<Transition> list = distributionMap.get(s);
			float occurencies = (float) computeTotalOccurrencies(list);
			body += "[] s=" + String.valueOf(stateMap.get(s)) + " -> ";
			for (Transition t : list) {
				body += ((float)t.getOccurrences())/occurencies + " : ( s'="
						+ stateMap.get(t.getDestination())+" )";
				if(list.indexOf(t)==list.size()-1){
					body +=";";
				}else
					body +=" + ";
			}
			body += "\n";
		}
		return labels + header + body + footer;
	}
	
	private static int computeTotalOccurrencies(List<Transition> transitions){
		int occurences = 0;
		for (Transition t : transitions) {
			occurences += t.getOccurrences();
		}
		return occurences;
	}

	private static String createHeader(int size, int init) {
		String header = "\n\nmodule logfile\n\n";
		header += "s : [0.." + size + "] init "+init+";\n\n";
		return header;
	}
}
